fix(pkg): compare compiler packages semantically - #16173

## Summary

- Build one SAT universe containing every requested platform instead of
solving each platform independently.
- Make roles, availability, conflict classes, and result extraction
platform-aware.
- Constrain every platform role for a package to select the same
version, choosing an older common version when necessary and failing
when no common version exists.
- Resolve each platform's package formulas against only the packages
selected on that platform, preserving platform-specific dependency
alternatives.
- Generate conditional lock-file data directly from the joint result and
remove obsolete result-merging APIs.
- Keep diagnostics origin-aware: repository pre-rejections are reported
only for repository-backed roles, and failures affecting a subset of
requested platforms retain their platform qualifiers.
- Remove the unreachable warning path for non-boolean availability
filters, which are treated as unavailable.
- Credit: the cross-platform version-equality SAT encoding was proposed
by @art-w in #13647.

This branch is rebased on `main` after #16210 landed. It does not
include #16172 or #16173.

## Landed preparation

The following independent preparatory PRs have landed on `main`.

### Observability and solver invariants

- #15923 adds the opt-in SAT trace category and `sat/solve` statistics.
- #15961 records solve counts and statistics in the existing solver
tests.
- #15962 snapshots all-or-nothing failure, deduplicated manifest errors,
and the legacy per-platform version divergence.
- #15981 makes portable lock-directory generation all-or-nothing before
changing the solver architecture.

### Per-platform semantics

- #15998 preserves per-platform dependency-alternative selections.
- #15999 preserves platform filters in local package constraints.
- #16000 preserves platform-specific rejection reasons.
- #16001 records legacy per-platform version selection.
- #16002 covers extra files when platforms converge on a common version.
- #16003 preserves the single-platform SAT problem size.
- #16009 preserves legacy dependencies whose names overlap formula
constructors.
- #16010 preserves platform-local conflict-class diagnostics.

### Joint-solve edge cases

- #16040 covers a solvable portable platform set.
- #16041 reproduces duplicate-platform failures.
- #16042 records per-platform avoid minimization.
- #16057 preserves platform-specific alternatives selected for local
package dependencies.
- #16058 ignores malformed repository versions excluded by local
constraints.
- #16084 preserves post-dependency reachability independently for each
platform.
- #16210 records per-platform diagnostic behavior for one-of-many and
two-of-four failures, platform-dependent pin availability, repository
versions shadowed by pins, and non-boolean availability filters.

### Build and tool integration

- #16167 snapshots host-platform package selection in build contexts.
- #16168 covers dev-tool compiler-package relocking and lock reuse.
- #16169 snapshots the former precedence between explicit
`solve_for_platforms` entries and conflicting lock-stanza solver
variables.

## Independent related fixes

The following sibling PRs are based directly on `main` and are not
dependencies of this PR:

- #16172 rejects solver variables repeated across lock-stanza
environment fields and honors valid lock-stanza environments during
package builds.
- #16173 compares project and dev-tool compiler packages semantically,
avoiding unnecessary relocking while preserving same-version
recipe-change detection.

## Review fixes

- Compute post-solve reachability separately for every platform before
taking the union, so a local package's macOS alternative is not dropped
after its Linux alternative is visited first.
- Keep versions rejected on every platform out of manifest loading,
while retaining platform-local candidates needed by another platform.
- Do not attach repository pre-rejections to local or pinned roles,
whose repository versions are not candidates.
- Preserve platform annotations whenever a failure affects fewer than
all requested platforms, including identical failures on two of four
platforms.
- Report cross-platform version conflicts with the selected version and
platform instead of an opaque SAT clause.
- Rename and rewrite the no-common-version regression so its name and
prose match the enforced invariant.
- Remove the redundant platform-version extra-files regression at the
commit where joint version equality makes it obsolete.
- Avoid constructing a discarded non-portable platform input and remove
the unreachable non-boolean availability warning.

## Checks

- `dune runtest test/blackbox-tests/test-cases/pkg/portable-lockdirs`
- `CI=true dune build @fmt @check`

Closes #13647